A:Type, eq,P:top. fpf-all(A; eq; fpf-empty; y,w.P(y,w))  True 

latex

Definitions	top, fpf-empty, fpf-all(A; eq; f; x,v.P(x;v)), fpf-dom(eq; x; f), b, P  Q, P  Q, P  Q, x:A. B(x), P  Q, x(s1,s2), False, t  T, True
Lemmas	true wf, false wf, top wf